Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems
Identifieur interne : 00BC31 ( Main/Exploration ); précédent : 00BC30; suivant : 00BC32Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems
Auteurs : Alfons Geser [Allemagne]Source :
- Journal of Symbolic Computation [ 0747-7171 ] ; 1997.
English descriptors
- Teeft :
- Academic press, Cancellation rule, Decimal digits, Digit, Function symbol, Function symbols, Geser, Geser proof, Ground instance, Ground term, Ground terms, Integer, Interpretation orders, Lenf, Monotonic, Monotonic interpretation, Monotonic interpretations, Orders subterms, Ordinal numbers, Positive integer number, Positive integer numbers, Positive integers, Post correspondence problem, Prec, Reduction length, Reduction lengths, Reduction order, Revc, Simple termination, Strict monotonicity, Structural induction, Symbolic computation, Termination, Termination type, Total reduction order, Total reduction orders, Total termination, Trss, Turing machines, Unbarred letters, Undecidable, Upper bounds, Zantema.
Abstract
Abstract: We give a complete proof of the fact that the following problem is undecidable:Given:A term rewriting system, where the termination of its rewrite relation is provable by a total reduction order on ground terms,Wanted:Does there exist a strictly monotonic interpretation in the positive integers that proves termination?
Url:
DOI: 10.1006/jsco.1996.0095
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002C02
- to stream Istex, to step Curation: 002B65
- to stream Istex, to step Checkpoint: 002764
- to stream Main, to step Merge: 00C409
- to stream Main, to step Curation: 00BC31
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems</title><author><name sortKey="Geser, Alfons" sort="Geser, Alfons" uniqKey="Geser A" first="Alfons" last="Geser">Alfons Geser</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B976A1163A02D2F06BFEB28724F31495FCA3832E</idno><date when="1997" year="1997">1997</date><idno type="doi">10.1006/jsco.1996.0095</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-NJ8LLN67-C/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002C02</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002C02</idno><idno type="wicri:Area/Istex/Curation">002B65</idno><idno type="wicri:Area/Istex/Checkpoint">002764</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002764</idno><idno type="wicri:doubleKey">0747-7171:1997:Geser A:omega:termination:is</idno><idno type="wicri:Area/Main/Merge">00C409</idno><idno type="wicri:Area/Main/Curation">00BC31</idno><idno type="wicri:Area/Main/Exploration">00BC31</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems</title><author><name sortKey="Geser, Alfons" sort="Geser, Alfons" uniqKey="Geser A" first="Alfons" last="Geser">Alfons Geser</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Wilhelm-Schickard-Institut für Informatik, Universität Tübingen, Sand 13, Tübingen, D-72076</wicri:regionArea><placeName><region type="land" nuts="1">Bade-Wurtemberg</region><region type="district" nuts="2">District de Tübingen</region><settlement type="city">Tübingen</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Symbolic Computation</title><title level="j" type="abbrev">YJSCO</title><idno type="ISSN">0747-7171</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1997">1997</date><biblScope unit="volume">23</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="399">399</biblScope><biblScope unit="page" to="411">411</biblScope></imprint><idno type="ISSN">0747-7171</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0747-7171</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Academic press</term><term>Cancellation rule</term><term>Decimal digits</term><term>Digit</term><term>Function symbol</term><term>Function symbols</term><term>Geser</term><term>Geser proof</term><term>Ground instance</term><term>Ground term</term><term>Ground terms</term><term>Integer</term><term>Interpretation orders</term><term>Lenf</term><term>Monotonic</term><term>Monotonic interpretation</term><term>Monotonic interpretations</term><term>Orders subterms</term><term>Ordinal numbers</term><term>Positive integer number</term><term>Positive integer numbers</term><term>Positive integers</term><term>Post correspondence problem</term><term>Prec</term><term>Reduction length</term><term>Reduction lengths</term><term>Reduction order</term><term>Revc</term><term>Simple termination</term><term>Strict monotonicity</term><term>Structural induction</term><term>Symbolic computation</term><term>Termination</term><term>Termination type</term><term>Total reduction order</term><term>Total reduction orders</term><term>Total termination</term><term>Trss</term><term>Turing machines</term><term>Unbarred letters</term><term>Undecidable</term><term>Upper bounds</term><term>Zantema</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We give a complete proof of the fact that the following problem is undecidable:Given:A term rewriting system, where the termination of its rewrite relation is provable by a total reduction order on ground terms,Wanted:Does there exist a strictly monotonic interpretation in the positive integers that proves termination?</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Bade-Wurtemberg</li><li>District de Tübingen</li></region><settlement><li>Tübingen</li></settlement></list><tree><country name="Allemagne"><region name="Bade-Wurtemberg"><name sortKey="Geser, Alfons" sort="Geser, Alfons" uniqKey="Geser A" first="Alfons" last="Geser">Alfons Geser</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00BC31 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00BC31 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:B976A1163A02D2F06BFEB28724F31495FCA3832E
|texte= Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems
}}
| This area was generated with Dilib version V0.6.33. |  |